Specification array-indices

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,
enrich
   nat-list-less
, 
   array-copy

with
   

   
   
   functions  . .indicesWhere ( . ) : array × (elem → bool) → nat-list;
              . .indicesWhere ( . ) : array × (elem → bool) × nat → nat-list;
              . .mapIndices ( . ) : array × nat-list × (elem → elem) → array;
              . .mapIndices ( . ) : array × nat-set × (elem → elem) → array;
              . .mapIf ( . ) : array × (elem → bool) × (elem → elem) → array;
              . .mapIf ( . ) : array × (elem → bool) × (elem → elem) × nat → array;
              . .map ( . ) : nat-set × (nat → nat) → nat-set;
              . .map ( . ) : array × (elem → elem) → array;
              . .filter ( . ) : nat-set × (nat → bool) → nat-set;
   predicates  valid-indices : array × nat-list;
   
   variables  φ : elem → bool;
              φn : nat → bool;
              f : elem → elem;
              fn : nat → nat;
   
   

   

   axioms indiceswhere-base :  ⊦ ar.indicesWhere(φ, 0) = [];
          used for: s, ls;
          indiceswhere-rec :  ⊦ n < # ar → ar.indicesWhere(φ, n + 1) = ar.indicesWhere(φ, n) + (φ(ar[n]) ⊃ n + [];[]);
          used for: ls;
          indiceswhere :  ⊦ ar.indicesWhere(φ) = ar.indicesWhere(φ, # ar);
          valid-indices :  ⊦ valid-indices(ar, nx) ↔ nx < # ar;
          used for: ls;
          mapindices-base :  ⊦ ar.mapIndices([], f) = ar;
          used for: s, ls;
          mapindices-rec :  ⊦ n < # ar → ar.mapIndices(n ' + nx, f) = (n < # ar ⊃ ar[n, f(ar[n])];ar).mapIndices(nx, f);
          used for: s, ls;
          mapindices-size :  ⊦ # ar.mapIndices(ns, f) = # ar;
          used for: s, ls;
          mapindices-at :  ⊦ ar.mapIndices(ns, f)[n] = (n ∈ ns ∧ n < # ar ⊃ f(ar[n]);ar[n]);
          used for: ls;
          mapif-def :  ⊦ ar.mapIf(φ, f) = ar.mapIndices(ar.indicesWhere(φ), f);
          mapifn-def :  ⊦ ar.mapIf(φ, f, n) = ar.mapIndices(ar.indicesWhere(φ, n), f);
          map-size :  ⊦ # ar.map(f) = # ar;
          used for: s, ls;
          map-at :  ⊦ ar.map(f)[n] = (n < # ar ⊃ f(ar[n]);ar[n]);
          used for: ls;
          mapset-def :  ⊦ n ∈ ns.map(fn) ↔ (∃ n0. n = fn(n0) ∧ n0 ∈ ns);
          used for: ls;
          filterset-def :  ⊦ n ∈ ns.filter(φn) ↔ n ∈ ns ∧ φn(n);
          used for: s, ls;

   

   
end enrich